Nuprl Lemma : exists_functionality_wrt_iff
9,38
postcript
pdf
S
,
T
:Type,
P
,
Q
:(
S
). (
S
=
T
)
(
x
:
S
.
P
(
x
)
Q
(
x
))
((
x
:
S
.
P
(
x
))
(
y
:
T
.
Q
(
y
)))
latex
ProofTree
Definitions
t
T
,
P
Q
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
P
Q
,
P
Q
,
,
x
:
A
.
B
(
x
)
Lemmas
iff
wf
origin
S,T:Type, P,Q:(S
). (S = T) 
(x:S. P(x) 
Q(x)) ((
x:S. P(x)) (y:T. Q(y)))
S,T:Type, P,Q:(S). (S = T) (x:S. P(x) Q(x)) ((x:S. P(x)) (y:T. Q(y)))
T Q
Qx:A. B(x) Q Qx:A. B(x)